\chapter{分布式数据平面验证的计算模型研究}
\section{数据平面验证相关元素定义}
\begin{definition}
数据包头（packet header）：一个数据包头$h \in \{0,1\}^{l}$构成一个比特序列，$l$为该比特序列的长度。
\end{definition}

由于网络往往根据特定的路由协议工作，路由协议只关心其对应数据包头的某一部分，在没有特别说明情况下，本文中的数据包头指代协议相关部分，如IP网络中目的地址为1.2.3.4的数据包头$h=\{00000001\ 00000010\ 00000011\ 00000100\}$。

\begin{definition}
  包头空间（header space）: 数据包头空间$H=\{h_1,...,h_{|H|}\}$是由数据包头构成的集合，且$\forall h_i,h_j \in H: h_i \neq h_j$。
\end{definition}

令$\mathbb{H}=\{0,1\}^l$为长度为$l$的所有可能的包头构成的全集，对于数据包头空间$H_1,H_2\in 2^\mathbb{H}$，本文定义以下操作符：

\begin{equation}
\begin{split}
  H_1 \times H_2 = H_1 \wedge H_2\\
  H_1 + H_2 = H_1 \vee H_2
\end{split}
\end{equation}


根据集合的代数特性，$2^\mathbb{H}$构成一个环$\langle 2^\mathbb{H},\times,+\rangle$，上述操作符满足交换律、结合律和分配律：
\begin{equation}
% \begin{gather*}
\begin{split}
  H_1 \times H_2 = H_2 \times H_1 \\
  H_1 + H_2 = H_2 + H_1 \\
  H_1 \times H_2 \times H_3=H_1 \times (H_2 \times H_3 )\\
  H_1+H_2+H_3=H_1+(H_2+H_3 )\\
  H_1 \times (H_2+H_3 )=H_1 \times H_2+H_2 \times H_3
\end{split}
% \end{gather*}
\end{equation}

\begin{definition}
  转发信息表(FIB)。一个转发信息表为一个元组$T=\{PRI,\Sigma,\epsilon,F\}$，其中$PRI \subset \mathbb{N}$为优先级集合，$\Sigma\subset \mathbb{H}$为包头空间集合，$\epsilon \subset E$为拓扑抽象的边集合，$F:PRI \times \Sigma \rightarrow \epsilon \times \Sigma$为数据包转发函数。
  
  包含一系列数据包转发规则，每条规则$r(pri,m,\epsilon,\eta)\in T$为一个key-value pair $\mathbb{N} \times 2^\mathbb{H} \rightarrow 2^E \times \mathbb{H}$。令$r=$
\end{definition}

\begin{definition}
  定位数据包头（Located packet header）。给定一个数据包头$h \in \mathbb{H}$和一个网络设备$v \in V$，$L_{h,v} \in \mathbb{H} \times V$为一个定位数据包头。
\end{definition}

\begin{definition}
  定位包头空间（Located header space）。给定一个包头空间$H \in 2^\mathbb{H}$和一个网络设备$v \in V$，$L_{H,v} \in 2^\mathbb{H} \times V$为一个定位包头空间。
\end{definition}

\begin{definition}
  Packet trace。给定一个初始的定位数据包$L_{h,v}$，该数据包经过网络路由生成一个定位数据包序列$L_{h,v}^*$，我们称该序列为$L_{h,v}$的packet trace。
\end{definition}

\begin{definition}
  Header space trace。给定一个初始的定位包头空间$L_{H,v}$，$\forall l \in \{L_{h,v} | h \in H\}$经过网络路由后生成一个定位数据包序列集合$\{L_{h,v}^*\}^{|H|}$，我们称该序列集合为$L_{H,v}$的header space trace。
\end{definition}

\section{数据平面验证的基本概念抽象}
\subsection{物理网络抽象}
一个物理网络抽象为一个元组$Net(V,E,R)$，其中$V$为物理网络中的所有网络设备，$E \subset V \times V$为一组有向边，网络中每条物理连接对应两条方向相反的有向边，对于边$e(u,v)$，我们定义$src(e)=u$和$dst(e)=v$。$R \subset \mathbb{N} \times 2^H \times 2^{E \times RW}$为物理网络中所有的转发规则，其中$RW: H \rightarrow H$为数据包重写函数。



一个物理网络包含多个网络设备和链接，我们将其抽象为一个有向图$G(V,E)$，其中$V$为物理网络中的所有网络设备，网络中每条链接对应$E$中两条方向相反的有向边。每个网络设备$v \in V$包含多个端口$P_v=\{P_v^1,P_v^2,\dots\}$，每个端口对应于连接到$v$的其中一条出边。

每个网络设备$v \in V$包含一套转发信息表（FIB）$T$，表中包含一系列数据包转发规则，每条规则$r\in T$可抽象为一个三元组$\langle pri, match, action \rangle$, 其中$pri \in \mathbb{Z}$为该规则的优先级，$match \in \{0,1,x\}^L$为数据包头的匹配值，$x$为任意匹配，$L$为数据包头长度，$action$为对应的动作，如转发、多播、广播或者丢弃。FIB的语义如下，对于包头为$h$的数据包进入交换机，如果某条规则$r$的$match$域能够匹配$h$，且该规则是匹配$h$的最高优先级规则，则使用$r.action$来对该数据包进行处理。由于规则优先级的存在，具有相同语义的两个FIB可能会有不同的结构。

\begin{definition}
  FIB的等价性。对于两个FIB $T_1$和$T_2$，如果二者具有相同的转发语义，则二者是等价的，记为$T_1 \sim T_2$.
\end{definition}

\begin{definition}
  FIB的谓词形式：给定任意一个FIB $T$，其谓词形式$\mathcal{T}$为一个二元组集合$\mathcal{T}=\{\langle p_1,a_1 \rangle,...,\langle p_n,a_n \rangle\}$，其中$p_i$为一个谓词，$a_i$为对应的动作。
\end{definition}
FIB的谓词形式具有如下特性：
\begin{enumerate}
  \item $p_i \wedge p_j = False$ iff $i \neq j$;
  \item $\bigvee_{i=1}^n p_i = True$;
  \item $a_i \neq a_j$ iff $i \neq j$;
\end{enumerate}

\begin{theorem}
\label{the:predFIBequ}
  对于两个FIB $T_1$和$T_2$，如果$T_1 \sim  T_2$，则$\mathcal{T}_1 = \mathcal{T}_2$。
\end{theorem}
\begin{proof}
  若$\mathcal{T}_1 \neq \mathcal{T}_2$，则$\exists \langle p_i,a_i \rangle \in \mathcal{T}_1: p_i \wedge h \neq False$， $\exists \langle p_j,a_j \rangle \in \mathcal{T}_2: p_j \wedge h \neq False$，且$a_i \neq a_j$，那么意味着$\mathcal{T}_1$和$\mathcal{T}_2$具有不同转发语义，则$T_1$和$T_2$具有不同语义，与前提矛盾。
\end{proof}

\begin{theorem}
  对于具有相同语义的FIB族$\mathbb{T}=\{T_1,...,T_n\}$，$T_1 \sim T_2 \sim ... \sim T_n$，该FIB族的谓词形式是唯一的。
\end{theorem}
\begin{proof}
  根据定理~\ref{the:predFIBequ}，$\mathcal{T}_1 = \mathcal{T}_2=...=\mathcal{T}_n$，则$\mathbb{T}$中所有元素对应同一个谓词形式。
\end{proof}

\subsection{数据平面行为抽象}
网络的数据平面能够对进入网络的数据包进行转发和变换操作，我们称该过程位网络数据平面的动态行为。为了形式化描述网络的动态行为，我们定义以下基本概念。



\begin{definition}
  包头空间路由状态（header space routing state）LP:定义为一个二元组$\langle H,loc \rangle$，其中$H$为包头空间，$loc \in V$为当前网络位置。
\end{definition}

数据平面的动态行为可以抽象为对包头空间路由状态的变换。

一个物理网络$G(V,E)$的数据平面抽象为一个元组$D(G,H,R)$，其中$H$为网络所使用的路由协议对应的全部包头集合，$R\subset \mathbb{N} \times 2^H \times 2^E \times 2^{H\rightarrow H}$为网络设备所有的转发规则。对任意一条规则$r(pri,m,e,\tau) \in R$满足以下条件：
\begin{enumerate}
  \item 
\end{enumerate}

\subsection{数据平面验证的数据集抽象}
数据平面验证的数据集为一个元组$D=\{V,E,F\}$。其中$V$和$E$为拓扑抽象，$F$为一个key-value pair集合，其中key为一个三元组$key \in V \times \mathbb{Z} \times 2^\mathcal{H}$，而value为数据平面规则的动作。为了消除相同语义数据集的表达方式差异，数据集的键可以转换为谓词形式$key \in V \times \mathbb{P}$，从而消除了优先级。如图~\ref{fig:network}为一个包含三个设备的网络，各设备的FIB在图中列出，其对应的数据平面数据集抽象如图~\ref{fig:network-datset}所示。

\begin{figure}[htbp]
  \centering
  \includegraphics[width=\textwidth]{example-network.pdf}
  \caption{示例网络及其数据平面配置}
  \label{fig:network}
\end{figure}

\begin{figure}[htbp]
  \centering
  \includegraphics[width=.4\textwidth]{example-network-dataset.pdf}
  \caption{示例网络的数据集抽象}
  \label{fig:network-datset}
\end{figure}

\section{集中式数据平面验证模型}
在讨论分布式数据平面验证之前，我们先探讨集中式数据平面验证，然后对其进行分布式化。

\section{分布式数据平面验证计算模型}
分布式数据平面验证的计算模型依赖于数据划分方式，当前主要有两种划分方式。一种是基于包头空间划分，另一种是基于设备空间划分。对应于两种不同的分布式数据平面模型和验证计算模型。


\subsection{基于包头空间划分的分布式验证计算模型}
基于包头空间划分的分布式验证将包头空间$H$划分为$n$个互不相交的包头子空间$I=\{H_1,...,H_n\}$，每个计算实例负责其中一个包头子空间的验证。对于某个网络策略验证需求$req(H,path)$，$valid(req, D) = True \Leftrightarrow \bigwedge_{i \in I(H)} valid(req, i)$，其中$I(H)$为对于包头空间与$H$有交集的实例，即$i.H \wedge H \neq False$, $\forall i \in I$。